es:ES, e3, e2, e1:E. e1  e2   e1  e3   ([e1, e2]  [e1, e3]  e2  e3 ) 

latex

Definitions

x:A. B(x), P  Q, t  T, Prop, x. t(x), P  Q, P  Q, P & Q, e  e' , P  Q, {T}, A & B, A, T, True, WellFnd{i}(A;x,y.R(x;y)), x(s), (e <loc e'), False

Lemmas

es-locl-wellfnd, es-E wf, es-le wf, iff wf, iseg wf, es-interval wf, es-locl wf, event system wf, es-le-iff, es-pred wf, es-pred-locl, es-interval-less, es-le-pred, iff functionality wrt iff, or functionality wrt iff, iseg append single, es-interval-one-one, es-interval-eq, es-le-antisymmetric, es-le-self, es-le-not-locl, es-le-loc, es-loc wf, squash wf, true wf, member-es-interval, iseg member, member singleton, es-loc-pred, es-locl-iff, not wf, assert wf, es-first wf, iseg weakening